Inference at * 1 
Iof proof for Lemma member-exists:



1. T : Type
2. L : T List
3. x:T. (x  L)
  (L = []) 

latex

 by DVar `L' 

latex

 1: 

 1: 2. x:T. (x  [])
 1:   ([] = [])
 2: 

 2: 2. u : T
 2: 3. v : T List
 2: 4. x:T. (x  [u / v])
 2:   ([u / v] = [])
 .

Definitions

type List